T:Type, x:T, l1,l2:(T List). (x  append(l1; l2))  ((x  l1)  (x  l2)) 

latex

Definitions	t  T, Y, append(as; bs), x:A. B(x), prop{i:l}, P  Q, P  Q, P  Q, P  Q, P  Q, x. t(x), False, A, A  B, ||as||, A c B, , x:A. B(x), (x  l), x(s)
Lemmas	l member wf, or functionality wrt iff, cons member, iff functionality wrt iff, all functionality wrt iff, append wf, iff wf